(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
quicksort(Cons(x, Cons(x', xs))) → part(x, Cons(x', xs))
quicksort(Cons(x, Nil)) → Cons(x, Nil)
quicksort(Nil) → Nil
partLt(x', Cons(x, xs)) → partLt[Ite][True][Ite](<(x, x'), x', Cons(x, xs))
partLt(x, Nil) → Nil
partGt(x', Cons(x, xs)) → partGt[Ite][True][Ite](>(x, x'), x', Cons(x, xs))
partGt(x, Nil) → Nil
app(Cons(x, xs), ys) → Cons(x, app(xs, ys))
app(Nil, ys) → ys
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
part(x, xs) → app(quicksort(partLt(x, xs)), Cons(x, quicksort(partGt(x, xs))))
goal(xs) → quicksort(xs)
The (relative) TRS S consists of the following rules:
<(S(x), S(y)) → <(x, y)
<(0, S(y)) → True
<(x, 0) → False
>(S(x), S(y)) → >(x, y)
>(0, y) → False
>(S(x), 0) → True
partLt[Ite][True][Ite](True, x', Cons(x, xs)) → Cons(x, partLt(x', xs))
partGt[Ite][True][Ite](True, x', Cons(x, xs)) → Cons(x, partGt(x', xs))
partLt[Ite][True][Ite](False, x', Cons(x, xs)) → partLt(x', xs)
partGt[Ite][True][Ite](False, x', Cons(x, xs)) → partGt(x', xs)
Rewrite Strategy: INNERMOST
(1) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.
(2) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
quicksort(Cons(x, Cons(x', xs))) → part(x, Cons(x', xs))
quicksort(Cons(x, Nil)) → Cons(x, Nil)
quicksort(Nil) → Nil
partLt(x', Cons(x, xs)) → partLt[Ite][True][Ite](<(x, x'), x', Cons(x, xs))
partLt(x, Nil) → Nil
partGt(x', Cons(x, xs)) → partGt[Ite][True][Ite](>(x, x'), x', Cons(x, xs))
partGt(x, Nil) → Nil
app(Cons(x, xs), ys) → Cons(x, app(xs, ys))
app(Nil, ys) → ys
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
part(x, xs) → app(quicksort(partLt(x, xs)), Cons(x, quicksort(partGt(x, xs))))
goal(xs) → quicksort(xs)
The (relative) TRS S consists of the following rules:
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False
>(S(x), S(y)) → >(x, y)
>(0', y) → False
>(S(x), 0') → True
partLt[Ite][True][Ite](True, x', Cons(x, xs)) → Cons(x, partLt(x', xs))
partGt[Ite][True][Ite](True, x', Cons(x, xs)) → Cons(x, partGt(x', xs))
partLt[Ite][True][Ite](False, x', Cons(x, xs)) → partLt(x', xs)
partGt[Ite][True][Ite](False, x', Cons(x, xs)) → partGt(x', xs)
Rewrite Strategy: INNERMOST
(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.
(4) Obligation:
Innermost TRS:
Rules:
quicksort(Cons(x, Cons(x', xs))) → part(x, Cons(x', xs))
quicksort(Cons(x, Nil)) → Cons(x, Nil)
quicksort(Nil) → Nil
partLt(x', Cons(x, xs)) → partLt[Ite][True][Ite](<(x, x'), x', Cons(x, xs))
partLt(x, Nil) → Nil
partGt(x', Cons(x, xs)) → partGt[Ite][True][Ite](>(x, x'), x', Cons(x, xs))
partGt(x, Nil) → Nil
app(Cons(x, xs), ys) → Cons(x, app(xs, ys))
app(Nil, ys) → ys
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
part(x, xs) → app(quicksort(partLt(x, xs)), Cons(x, quicksort(partGt(x, xs))))
goal(xs) → quicksort(xs)
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False
>(S(x), S(y)) → >(x, y)
>(0', y) → False
>(S(x), 0') → True
partLt[Ite][True][Ite](True, x', Cons(x, xs)) → Cons(x, partLt(x', xs))
partGt[Ite][True][Ite](True, x', Cons(x, xs)) → Cons(x, partGt(x', xs))
partLt[Ite][True][Ite](False, x', Cons(x, xs)) → partLt(x', xs)
partGt[Ite][True][Ite](False, x', Cons(x, xs)) → partGt(x', xs)
Types:
quicksort :: Cons:Nil → Cons:Nil
Cons :: S:0' → Cons:Nil → Cons:Nil
part :: S:0' → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
partLt :: S:0' → Cons:Nil → Cons:Nil
partLt[Ite][True][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
< :: S:0' → S:0' → True:False
partGt :: S:0' → Cons:Nil → Cons:Nil
partGt[Ite][True][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
> :: S:0' → S:0' → True:False
app :: Cons:Nil → Cons:Nil → Cons:Nil
notEmpty :: Cons:Nil → True:False
True :: True:False
False :: True:False
goal :: Cons:Nil → Cons:Nil
S :: S:0' → S:0'
0' :: S:0'
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0'2_0 :: S:0'
hole_True:False3_0 :: True:False
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_S:0'5_0 :: Nat → S:0'
(5) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
quicksort,
partLt,
<,
partGt,
>,
appThey will be analysed ascendingly in the following order:
partLt < quicksort
partGt < quicksort
app < quicksort
< < partLt
> < partGt
(6) Obligation:
Innermost TRS:
Rules:
quicksort(
Cons(
x,
Cons(
x',
xs))) →
part(
x,
Cons(
x',
xs))
quicksort(
Cons(
x,
Nil)) →
Cons(
x,
Nil)
quicksort(
Nil) →
NilpartLt(
x',
Cons(
x,
xs)) →
partLt[Ite][True][Ite](
<(
x,
x'),
x',
Cons(
x,
xs))
partLt(
x,
Nil) →
NilpartGt(
x',
Cons(
x,
xs)) →
partGt[Ite][True][Ite](
>(
x,
x'),
x',
Cons(
x,
xs))
partGt(
x,
Nil) →
Nilapp(
Cons(
x,
xs),
ys) →
Cons(
x,
app(
xs,
ys))
app(
Nil,
ys) →
ysnotEmpty(
Cons(
x,
xs)) →
TruenotEmpty(
Nil) →
Falsepart(
x,
xs) →
app(
quicksort(
partLt(
x,
xs)),
Cons(
x,
quicksort(
partGt(
x,
xs))))
goal(
xs) →
quicksort(
xs)
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
False>(
S(
x),
S(
y)) →
>(
x,
y)
>(
0',
y) →
False>(
S(
x),
0') →
TruepartLt[Ite][True][Ite](
True,
x',
Cons(
x,
xs)) →
Cons(
x,
partLt(
x',
xs))
partGt[Ite][True][Ite](
True,
x',
Cons(
x,
xs)) →
Cons(
x,
partGt(
x',
xs))
partLt[Ite][True][Ite](
False,
x',
Cons(
x,
xs)) →
partLt(
x',
xs)
partGt[Ite][True][Ite](
False,
x',
Cons(
x,
xs)) →
partGt(
x',
xs)
Types:
quicksort :: Cons:Nil → Cons:Nil
Cons :: S:0' → Cons:Nil → Cons:Nil
part :: S:0' → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
partLt :: S:0' → Cons:Nil → Cons:Nil
partLt[Ite][True][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
< :: S:0' → S:0' → True:False
partGt :: S:0' → Cons:Nil → Cons:Nil
partGt[Ite][True][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
> :: S:0' → S:0' → True:False
app :: Cons:Nil → Cons:Nil → Cons:Nil
notEmpty :: Cons:Nil → True:False
True :: True:False
False :: True:False
goal :: Cons:Nil → Cons:Nil
S :: S:0' → S:0'
0' :: S:0'
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0'2_0 :: S:0'
hole_True:False3_0 :: True:False
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_S:0'5_0 :: Nat → S:0'
Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil4_0(x))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))
The following defined symbols remain to be analysed:
<, quicksort, partLt, partGt, >, app
They will be analysed ascendingly in the following order:
partLt < quicksort
partGt < quicksort
app < quicksort
< < partLt
> < partGt
(7) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
<(
gen_S:0'5_0(
n7_0),
gen_S:0'5_0(
+(
1,
n7_0))) →
True, rt ∈ Ω(0)
Induction Base:
<(gen_S:0'5_0(0), gen_S:0'5_0(+(1, 0))) →RΩ(0)
True
Induction Step:
<(gen_S:0'5_0(+(n7_0, 1)), gen_S:0'5_0(+(1, +(n7_0, 1)))) →RΩ(0)
<(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) →IH
True
We have rt ∈ Ω(1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n0).
(8) Complex Obligation (BEST)
(9) Obligation:
Innermost TRS:
Rules:
quicksort(
Cons(
x,
Cons(
x',
xs))) →
part(
x,
Cons(
x',
xs))
quicksort(
Cons(
x,
Nil)) →
Cons(
x,
Nil)
quicksort(
Nil) →
NilpartLt(
x',
Cons(
x,
xs)) →
partLt[Ite][True][Ite](
<(
x,
x'),
x',
Cons(
x,
xs))
partLt(
x,
Nil) →
NilpartGt(
x',
Cons(
x,
xs)) →
partGt[Ite][True][Ite](
>(
x,
x'),
x',
Cons(
x,
xs))
partGt(
x,
Nil) →
Nilapp(
Cons(
x,
xs),
ys) →
Cons(
x,
app(
xs,
ys))
app(
Nil,
ys) →
ysnotEmpty(
Cons(
x,
xs)) →
TruenotEmpty(
Nil) →
Falsepart(
x,
xs) →
app(
quicksort(
partLt(
x,
xs)),
Cons(
x,
quicksort(
partGt(
x,
xs))))
goal(
xs) →
quicksort(
xs)
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
False>(
S(
x),
S(
y)) →
>(
x,
y)
>(
0',
y) →
False>(
S(
x),
0') →
TruepartLt[Ite][True][Ite](
True,
x',
Cons(
x,
xs)) →
Cons(
x,
partLt(
x',
xs))
partGt[Ite][True][Ite](
True,
x',
Cons(
x,
xs)) →
Cons(
x,
partGt(
x',
xs))
partLt[Ite][True][Ite](
False,
x',
Cons(
x,
xs)) →
partLt(
x',
xs)
partGt[Ite][True][Ite](
False,
x',
Cons(
x,
xs)) →
partGt(
x',
xs)
Types:
quicksort :: Cons:Nil → Cons:Nil
Cons :: S:0' → Cons:Nil → Cons:Nil
part :: S:0' → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
partLt :: S:0' → Cons:Nil → Cons:Nil
partLt[Ite][True][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
< :: S:0' → S:0' → True:False
partGt :: S:0' → Cons:Nil → Cons:Nil
partGt[Ite][True][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
> :: S:0' → S:0' → True:False
app :: Cons:Nil → Cons:Nil → Cons:Nil
notEmpty :: Cons:Nil → True:False
True :: True:False
False :: True:False
goal :: Cons:Nil → Cons:Nil
S :: S:0' → S:0'
0' :: S:0'
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0'2_0 :: S:0'
hole_True:False3_0 :: True:False
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_S:0'5_0 :: Nat → S:0'
Lemmas:
<(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → True, rt ∈ Ω(0)
Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil4_0(x))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))
The following defined symbols remain to be analysed:
partLt, quicksort, partGt, >, app
They will be analysed ascendingly in the following order:
partLt < quicksort
partGt < quicksort
app < quicksort
> < partGt
(10) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
partLt(
gen_S:0'5_0(
0),
gen_Cons:Nil4_0(
n324_0)) →
gen_Cons:Nil4_0(
0), rt ∈ Ω(1 + n324
0)
Induction Base:
partLt(gen_S:0'5_0(0), gen_Cons:Nil4_0(0)) →RΩ(1)
Nil
Induction Step:
partLt(gen_S:0'5_0(0), gen_Cons:Nil4_0(+(n324_0, 1))) →RΩ(1)
partLt[Ite][True][Ite](<(0', gen_S:0'5_0(0)), gen_S:0'5_0(0), Cons(0', gen_Cons:Nil4_0(n324_0))) →RΩ(0)
partLt[Ite][True][Ite](False, gen_S:0'5_0(0), Cons(0', gen_Cons:Nil4_0(n324_0))) →RΩ(0)
partLt(gen_S:0'5_0(0), gen_Cons:Nil4_0(n324_0)) →IH
gen_Cons:Nil4_0(0)
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(11) Complex Obligation (BEST)
(12) Obligation:
Innermost TRS:
Rules:
quicksort(
Cons(
x,
Cons(
x',
xs))) →
part(
x,
Cons(
x',
xs))
quicksort(
Cons(
x,
Nil)) →
Cons(
x,
Nil)
quicksort(
Nil) →
NilpartLt(
x',
Cons(
x,
xs)) →
partLt[Ite][True][Ite](
<(
x,
x'),
x',
Cons(
x,
xs))
partLt(
x,
Nil) →
NilpartGt(
x',
Cons(
x,
xs)) →
partGt[Ite][True][Ite](
>(
x,
x'),
x',
Cons(
x,
xs))
partGt(
x,
Nil) →
Nilapp(
Cons(
x,
xs),
ys) →
Cons(
x,
app(
xs,
ys))
app(
Nil,
ys) →
ysnotEmpty(
Cons(
x,
xs)) →
TruenotEmpty(
Nil) →
Falsepart(
x,
xs) →
app(
quicksort(
partLt(
x,
xs)),
Cons(
x,
quicksort(
partGt(
x,
xs))))
goal(
xs) →
quicksort(
xs)
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
False>(
S(
x),
S(
y)) →
>(
x,
y)
>(
0',
y) →
False>(
S(
x),
0') →
TruepartLt[Ite][True][Ite](
True,
x',
Cons(
x,
xs)) →
Cons(
x,
partLt(
x',
xs))
partGt[Ite][True][Ite](
True,
x',
Cons(
x,
xs)) →
Cons(
x,
partGt(
x',
xs))
partLt[Ite][True][Ite](
False,
x',
Cons(
x,
xs)) →
partLt(
x',
xs)
partGt[Ite][True][Ite](
False,
x',
Cons(
x,
xs)) →
partGt(
x',
xs)
Types:
quicksort :: Cons:Nil → Cons:Nil
Cons :: S:0' → Cons:Nil → Cons:Nil
part :: S:0' → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
partLt :: S:0' → Cons:Nil → Cons:Nil
partLt[Ite][True][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
< :: S:0' → S:0' → True:False
partGt :: S:0' → Cons:Nil → Cons:Nil
partGt[Ite][True][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
> :: S:0' → S:0' → True:False
app :: Cons:Nil → Cons:Nil → Cons:Nil
notEmpty :: Cons:Nil → True:False
True :: True:False
False :: True:False
goal :: Cons:Nil → Cons:Nil
S :: S:0' → S:0'
0' :: S:0'
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0'2_0 :: S:0'
hole_True:False3_0 :: True:False
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_S:0'5_0 :: Nat → S:0'
Lemmas:
<(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → True, rt ∈ Ω(0)
partLt(gen_S:0'5_0(0), gen_Cons:Nil4_0(n324_0)) → gen_Cons:Nil4_0(0), rt ∈ Ω(1 + n3240)
Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil4_0(x))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))
The following defined symbols remain to be analysed:
>, quicksort, partGt, app
They will be analysed ascendingly in the following order:
partGt < quicksort
app < quicksort
> < partGt
(13) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
>(
gen_S:0'5_0(
n937_0),
gen_S:0'5_0(
n937_0)) →
False, rt ∈ Ω(0)
Induction Base:
>(gen_S:0'5_0(0), gen_S:0'5_0(0)) →RΩ(0)
False
Induction Step:
>(gen_S:0'5_0(+(n937_0, 1)), gen_S:0'5_0(+(n937_0, 1))) →RΩ(0)
>(gen_S:0'5_0(n937_0), gen_S:0'5_0(n937_0)) →IH
False
We have rt ∈ Ω(1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n0).
(14) Complex Obligation (BEST)
(15) Obligation:
Innermost TRS:
Rules:
quicksort(
Cons(
x,
Cons(
x',
xs))) →
part(
x,
Cons(
x',
xs))
quicksort(
Cons(
x,
Nil)) →
Cons(
x,
Nil)
quicksort(
Nil) →
NilpartLt(
x',
Cons(
x,
xs)) →
partLt[Ite][True][Ite](
<(
x,
x'),
x',
Cons(
x,
xs))
partLt(
x,
Nil) →
NilpartGt(
x',
Cons(
x,
xs)) →
partGt[Ite][True][Ite](
>(
x,
x'),
x',
Cons(
x,
xs))
partGt(
x,
Nil) →
Nilapp(
Cons(
x,
xs),
ys) →
Cons(
x,
app(
xs,
ys))
app(
Nil,
ys) →
ysnotEmpty(
Cons(
x,
xs)) →
TruenotEmpty(
Nil) →
Falsepart(
x,
xs) →
app(
quicksort(
partLt(
x,
xs)),
Cons(
x,
quicksort(
partGt(
x,
xs))))
goal(
xs) →
quicksort(
xs)
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
False>(
S(
x),
S(
y)) →
>(
x,
y)
>(
0',
y) →
False>(
S(
x),
0') →
TruepartLt[Ite][True][Ite](
True,
x',
Cons(
x,
xs)) →
Cons(
x,
partLt(
x',
xs))
partGt[Ite][True][Ite](
True,
x',
Cons(
x,
xs)) →
Cons(
x,
partGt(
x',
xs))
partLt[Ite][True][Ite](
False,
x',
Cons(
x,
xs)) →
partLt(
x',
xs)
partGt[Ite][True][Ite](
False,
x',
Cons(
x,
xs)) →
partGt(
x',
xs)
Types:
quicksort :: Cons:Nil → Cons:Nil
Cons :: S:0' → Cons:Nil → Cons:Nil
part :: S:0' → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
partLt :: S:0' → Cons:Nil → Cons:Nil
partLt[Ite][True][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
< :: S:0' → S:0' → True:False
partGt :: S:0' → Cons:Nil → Cons:Nil
partGt[Ite][True][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
> :: S:0' → S:0' → True:False
app :: Cons:Nil → Cons:Nil → Cons:Nil
notEmpty :: Cons:Nil → True:False
True :: True:False
False :: True:False
goal :: Cons:Nil → Cons:Nil
S :: S:0' → S:0'
0' :: S:0'
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0'2_0 :: S:0'
hole_True:False3_0 :: True:False
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_S:0'5_0 :: Nat → S:0'
Lemmas:
<(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → True, rt ∈ Ω(0)
partLt(gen_S:0'5_0(0), gen_Cons:Nil4_0(n324_0)) → gen_Cons:Nil4_0(0), rt ∈ Ω(1 + n3240)
>(gen_S:0'5_0(n937_0), gen_S:0'5_0(n937_0)) → False, rt ∈ Ω(0)
Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil4_0(x))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))
The following defined symbols remain to be analysed:
partGt, quicksort, app
They will be analysed ascendingly in the following order:
partGt < quicksort
app < quicksort
(16) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
partGt(
gen_S:0'5_0(
0),
gen_Cons:Nil4_0(
n1266_0)) →
gen_Cons:Nil4_0(
0), rt ∈ Ω(1 + n1266
0)
Induction Base:
partGt(gen_S:0'5_0(0), gen_Cons:Nil4_0(0)) →RΩ(1)
Nil
Induction Step:
partGt(gen_S:0'5_0(0), gen_Cons:Nil4_0(+(n1266_0, 1))) →RΩ(1)
partGt[Ite][True][Ite](>(0', gen_S:0'5_0(0)), gen_S:0'5_0(0), Cons(0', gen_Cons:Nil4_0(n1266_0))) →LΩ(0)
partGt[Ite][True][Ite](False, gen_S:0'5_0(0), Cons(0', gen_Cons:Nil4_0(n1266_0))) →RΩ(0)
partGt(gen_S:0'5_0(0), gen_Cons:Nil4_0(n1266_0)) →IH
gen_Cons:Nil4_0(0)
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(17) Complex Obligation (BEST)
(18) Obligation:
Innermost TRS:
Rules:
quicksort(
Cons(
x,
Cons(
x',
xs))) →
part(
x,
Cons(
x',
xs))
quicksort(
Cons(
x,
Nil)) →
Cons(
x,
Nil)
quicksort(
Nil) →
NilpartLt(
x',
Cons(
x,
xs)) →
partLt[Ite][True][Ite](
<(
x,
x'),
x',
Cons(
x,
xs))
partLt(
x,
Nil) →
NilpartGt(
x',
Cons(
x,
xs)) →
partGt[Ite][True][Ite](
>(
x,
x'),
x',
Cons(
x,
xs))
partGt(
x,
Nil) →
Nilapp(
Cons(
x,
xs),
ys) →
Cons(
x,
app(
xs,
ys))
app(
Nil,
ys) →
ysnotEmpty(
Cons(
x,
xs)) →
TruenotEmpty(
Nil) →
Falsepart(
x,
xs) →
app(
quicksort(
partLt(
x,
xs)),
Cons(
x,
quicksort(
partGt(
x,
xs))))
goal(
xs) →
quicksort(
xs)
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
False>(
S(
x),
S(
y)) →
>(
x,
y)
>(
0',
y) →
False>(
S(
x),
0') →
TruepartLt[Ite][True][Ite](
True,
x',
Cons(
x,
xs)) →
Cons(
x,
partLt(
x',
xs))
partGt[Ite][True][Ite](
True,
x',
Cons(
x,
xs)) →
Cons(
x,
partGt(
x',
xs))
partLt[Ite][True][Ite](
False,
x',
Cons(
x,
xs)) →
partLt(
x',
xs)
partGt[Ite][True][Ite](
False,
x',
Cons(
x,
xs)) →
partGt(
x',
xs)
Types:
quicksort :: Cons:Nil → Cons:Nil
Cons :: S:0' → Cons:Nil → Cons:Nil
part :: S:0' → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
partLt :: S:0' → Cons:Nil → Cons:Nil
partLt[Ite][True][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
< :: S:0' → S:0' → True:False
partGt :: S:0' → Cons:Nil → Cons:Nil
partGt[Ite][True][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
> :: S:0' → S:0' → True:False
app :: Cons:Nil → Cons:Nil → Cons:Nil
notEmpty :: Cons:Nil → True:False
True :: True:False
False :: True:False
goal :: Cons:Nil → Cons:Nil
S :: S:0' → S:0'
0' :: S:0'
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0'2_0 :: S:0'
hole_True:False3_0 :: True:False
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_S:0'5_0 :: Nat → S:0'
Lemmas:
<(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → True, rt ∈ Ω(0)
partLt(gen_S:0'5_0(0), gen_Cons:Nil4_0(n324_0)) → gen_Cons:Nil4_0(0), rt ∈ Ω(1 + n3240)
>(gen_S:0'5_0(n937_0), gen_S:0'5_0(n937_0)) → False, rt ∈ Ω(0)
partGt(gen_S:0'5_0(0), gen_Cons:Nil4_0(n1266_0)) → gen_Cons:Nil4_0(0), rt ∈ Ω(1 + n12660)
Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil4_0(x))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))
The following defined symbols remain to be analysed:
app, quicksort
They will be analysed ascendingly in the following order:
app < quicksort
(19) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
app(
gen_Cons:Nil4_0(
n2032_0),
gen_Cons:Nil4_0(
b)) →
gen_Cons:Nil4_0(
+(
n2032_0,
b)), rt ∈ Ω(1 + n2032
0)
Induction Base:
app(gen_Cons:Nil4_0(0), gen_Cons:Nil4_0(b)) →RΩ(1)
gen_Cons:Nil4_0(b)
Induction Step:
app(gen_Cons:Nil4_0(+(n2032_0, 1)), gen_Cons:Nil4_0(b)) →RΩ(1)
Cons(0', app(gen_Cons:Nil4_0(n2032_0), gen_Cons:Nil4_0(b))) →IH
Cons(0', gen_Cons:Nil4_0(+(b, c2033_0)))
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(20) Complex Obligation (BEST)
(21) Obligation:
Innermost TRS:
Rules:
quicksort(
Cons(
x,
Cons(
x',
xs))) →
part(
x,
Cons(
x',
xs))
quicksort(
Cons(
x,
Nil)) →
Cons(
x,
Nil)
quicksort(
Nil) →
NilpartLt(
x',
Cons(
x,
xs)) →
partLt[Ite][True][Ite](
<(
x,
x'),
x',
Cons(
x,
xs))
partLt(
x,
Nil) →
NilpartGt(
x',
Cons(
x,
xs)) →
partGt[Ite][True][Ite](
>(
x,
x'),
x',
Cons(
x,
xs))
partGt(
x,
Nil) →
Nilapp(
Cons(
x,
xs),
ys) →
Cons(
x,
app(
xs,
ys))
app(
Nil,
ys) →
ysnotEmpty(
Cons(
x,
xs)) →
TruenotEmpty(
Nil) →
Falsepart(
x,
xs) →
app(
quicksort(
partLt(
x,
xs)),
Cons(
x,
quicksort(
partGt(
x,
xs))))
goal(
xs) →
quicksort(
xs)
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
False>(
S(
x),
S(
y)) →
>(
x,
y)
>(
0',
y) →
False>(
S(
x),
0') →
TruepartLt[Ite][True][Ite](
True,
x',
Cons(
x,
xs)) →
Cons(
x,
partLt(
x',
xs))
partGt[Ite][True][Ite](
True,
x',
Cons(
x,
xs)) →
Cons(
x,
partGt(
x',
xs))
partLt[Ite][True][Ite](
False,
x',
Cons(
x,
xs)) →
partLt(
x',
xs)
partGt[Ite][True][Ite](
False,
x',
Cons(
x,
xs)) →
partGt(
x',
xs)
Types:
quicksort :: Cons:Nil → Cons:Nil
Cons :: S:0' → Cons:Nil → Cons:Nil
part :: S:0' → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
partLt :: S:0' → Cons:Nil → Cons:Nil
partLt[Ite][True][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
< :: S:0' → S:0' → True:False
partGt :: S:0' → Cons:Nil → Cons:Nil
partGt[Ite][True][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
> :: S:0' → S:0' → True:False
app :: Cons:Nil → Cons:Nil → Cons:Nil
notEmpty :: Cons:Nil → True:False
True :: True:False
False :: True:False
goal :: Cons:Nil → Cons:Nil
S :: S:0' → S:0'
0' :: S:0'
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0'2_0 :: S:0'
hole_True:False3_0 :: True:False
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_S:0'5_0 :: Nat → S:0'
Lemmas:
<(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → True, rt ∈ Ω(0)
partLt(gen_S:0'5_0(0), gen_Cons:Nil4_0(n324_0)) → gen_Cons:Nil4_0(0), rt ∈ Ω(1 + n3240)
>(gen_S:0'5_0(n937_0), gen_S:0'5_0(n937_0)) → False, rt ∈ Ω(0)
partGt(gen_S:0'5_0(0), gen_Cons:Nil4_0(n1266_0)) → gen_Cons:Nil4_0(0), rt ∈ Ω(1 + n12660)
app(gen_Cons:Nil4_0(n2032_0), gen_Cons:Nil4_0(b)) → gen_Cons:Nil4_0(+(n2032_0, b)), rt ∈ Ω(1 + n20320)
Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil4_0(x))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))
The following defined symbols remain to be analysed:
quicksort
(22) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol quicksort.
(23) Obligation:
Innermost TRS:
Rules:
quicksort(
Cons(
x,
Cons(
x',
xs))) →
part(
x,
Cons(
x',
xs))
quicksort(
Cons(
x,
Nil)) →
Cons(
x,
Nil)
quicksort(
Nil) →
NilpartLt(
x',
Cons(
x,
xs)) →
partLt[Ite][True][Ite](
<(
x,
x'),
x',
Cons(
x,
xs))
partLt(
x,
Nil) →
NilpartGt(
x',
Cons(
x,
xs)) →
partGt[Ite][True][Ite](
>(
x,
x'),
x',
Cons(
x,
xs))
partGt(
x,
Nil) →
Nilapp(
Cons(
x,
xs),
ys) →
Cons(
x,
app(
xs,
ys))
app(
Nil,
ys) →
ysnotEmpty(
Cons(
x,
xs)) →
TruenotEmpty(
Nil) →
Falsepart(
x,
xs) →
app(
quicksort(
partLt(
x,
xs)),
Cons(
x,
quicksort(
partGt(
x,
xs))))
goal(
xs) →
quicksort(
xs)
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
False>(
S(
x),
S(
y)) →
>(
x,
y)
>(
0',
y) →
False>(
S(
x),
0') →
TruepartLt[Ite][True][Ite](
True,
x',
Cons(
x,
xs)) →
Cons(
x,
partLt(
x',
xs))
partGt[Ite][True][Ite](
True,
x',
Cons(
x,
xs)) →
Cons(
x,
partGt(
x',
xs))
partLt[Ite][True][Ite](
False,
x',
Cons(
x,
xs)) →
partLt(
x',
xs)
partGt[Ite][True][Ite](
False,
x',
Cons(
x,
xs)) →
partGt(
x',
xs)
Types:
quicksort :: Cons:Nil → Cons:Nil
Cons :: S:0' → Cons:Nil → Cons:Nil
part :: S:0' → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
partLt :: S:0' → Cons:Nil → Cons:Nil
partLt[Ite][True][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
< :: S:0' → S:0' → True:False
partGt :: S:0' → Cons:Nil → Cons:Nil
partGt[Ite][True][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
> :: S:0' → S:0' → True:False
app :: Cons:Nil → Cons:Nil → Cons:Nil
notEmpty :: Cons:Nil → True:False
True :: True:False
False :: True:False
goal :: Cons:Nil → Cons:Nil
S :: S:0' → S:0'
0' :: S:0'
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0'2_0 :: S:0'
hole_True:False3_0 :: True:False
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_S:0'5_0 :: Nat → S:0'
Lemmas:
<(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → True, rt ∈ Ω(0)
partLt(gen_S:0'5_0(0), gen_Cons:Nil4_0(n324_0)) → gen_Cons:Nil4_0(0), rt ∈ Ω(1 + n3240)
>(gen_S:0'5_0(n937_0), gen_S:0'5_0(n937_0)) → False, rt ∈ Ω(0)
partGt(gen_S:0'5_0(0), gen_Cons:Nil4_0(n1266_0)) → gen_Cons:Nil4_0(0), rt ∈ Ω(1 + n12660)
app(gen_Cons:Nil4_0(n2032_0), gen_Cons:Nil4_0(b)) → gen_Cons:Nil4_0(+(n2032_0, b)), rt ∈ Ω(1 + n20320)
Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil4_0(x))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))
No more defined symbols left to analyse.
(24) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
partLt(gen_S:0'5_0(0), gen_Cons:Nil4_0(n324_0)) → gen_Cons:Nil4_0(0), rt ∈ Ω(1 + n3240)
(25) BOUNDS(n^1, INF)
(26) Obligation:
Innermost TRS:
Rules:
quicksort(
Cons(
x,
Cons(
x',
xs))) →
part(
x,
Cons(
x',
xs))
quicksort(
Cons(
x,
Nil)) →
Cons(
x,
Nil)
quicksort(
Nil) →
NilpartLt(
x',
Cons(
x,
xs)) →
partLt[Ite][True][Ite](
<(
x,
x'),
x',
Cons(
x,
xs))
partLt(
x,
Nil) →
NilpartGt(
x',
Cons(
x,
xs)) →
partGt[Ite][True][Ite](
>(
x,
x'),
x',
Cons(
x,
xs))
partGt(
x,
Nil) →
Nilapp(
Cons(
x,
xs),
ys) →
Cons(
x,
app(
xs,
ys))
app(
Nil,
ys) →
ysnotEmpty(
Cons(
x,
xs)) →
TruenotEmpty(
Nil) →
Falsepart(
x,
xs) →
app(
quicksort(
partLt(
x,
xs)),
Cons(
x,
quicksort(
partGt(
x,
xs))))
goal(
xs) →
quicksort(
xs)
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
False>(
S(
x),
S(
y)) →
>(
x,
y)
>(
0',
y) →
False>(
S(
x),
0') →
TruepartLt[Ite][True][Ite](
True,
x',
Cons(
x,
xs)) →
Cons(
x,
partLt(
x',
xs))
partGt[Ite][True][Ite](
True,
x',
Cons(
x,
xs)) →
Cons(
x,
partGt(
x',
xs))
partLt[Ite][True][Ite](
False,
x',
Cons(
x,
xs)) →
partLt(
x',
xs)
partGt[Ite][True][Ite](
False,
x',
Cons(
x,
xs)) →
partGt(
x',
xs)
Types:
quicksort :: Cons:Nil → Cons:Nil
Cons :: S:0' → Cons:Nil → Cons:Nil
part :: S:0' → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
partLt :: S:0' → Cons:Nil → Cons:Nil
partLt[Ite][True][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
< :: S:0' → S:0' → True:False
partGt :: S:0' → Cons:Nil → Cons:Nil
partGt[Ite][True][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
> :: S:0' → S:0' → True:False
app :: Cons:Nil → Cons:Nil → Cons:Nil
notEmpty :: Cons:Nil → True:False
True :: True:False
False :: True:False
goal :: Cons:Nil → Cons:Nil
S :: S:0' → S:0'
0' :: S:0'
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0'2_0 :: S:0'
hole_True:False3_0 :: True:False
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_S:0'5_0 :: Nat → S:0'
Lemmas:
<(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → True, rt ∈ Ω(0)
partLt(gen_S:0'5_0(0), gen_Cons:Nil4_0(n324_0)) → gen_Cons:Nil4_0(0), rt ∈ Ω(1 + n3240)
>(gen_S:0'5_0(n937_0), gen_S:0'5_0(n937_0)) → False, rt ∈ Ω(0)
partGt(gen_S:0'5_0(0), gen_Cons:Nil4_0(n1266_0)) → gen_Cons:Nil4_0(0), rt ∈ Ω(1 + n12660)
app(gen_Cons:Nil4_0(n2032_0), gen_Cons:Nil4_0(b)) → gen_Cons:Nil4_0(+(n2032_0, b)), rt ∈ Ω(1 + n20320)
Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil4_0(x))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))
No more defined symbols left to analyse.
(27) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
partLt(gen_S:0'5_0(0), gen_Cons:Nil4_0(n324_0)) → gen_Cons:Nil4_0(0), rt ∈ Ω(1 + n3240)
(28) BOUNDS(n^1, INF)
(29) Obligation:
Innermost TRS:
Rules:
quicksort(
Cons(
x,
Cons(
x',
xs))) →
part(
x,
Cons(
x',
xs))
quicksort(
Cons(
x,
Nil)) →
Cons(
x,
Nil)
quicksort(
Nil) →
NilpartLt(
x',
Cons(
x,
xs)) →
partLt[Ite][True][Ite](
<(
x,
x'),
x',
Cons(
x,
xs))
partLt(
x,
Nil) →
NilpartGt(
x',
Cons(
x,
xs)) →
partGt[Ite][True][Ite](
>(
x,
x'),
x',
Cons(
x,
xs))
partGt(
x,
Nil) →
Nilapp(
Cons(
x,
xs),
ys) →
Cons(
x,
app(
xs,
ys))
app(
Nil,
ys) →
ysnotEmpty(
Cons(
x,
xs)) →
TruenotEmpty(
Nil) →
Falsepart(
x,
xs) →
app(
quicksort(
partLt(
x,
xs)),
Cons(
x,
quicksort(
partGt(
x,
xs))))
goal(
xs) →
quicksort(
xs)
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
False>(
S(
x),
S(
y)) →
>(
x,
y)
>(
0',
y) →
False>(
S(
x),
0') →
TruepartLt[Ite][True][Ite](
True,
x',
Cons(
x,
xs)) →
Cons(
x,
partLt(
x',
xs))
partGt[Ite][True][Ite](
True,
x',
Cons(
x,
xs)) →
Cons(
x,
partGt(
x',
xs))
partLt[Ite][True][Ite](
False,
x',
Cons(
x,
xs)) →
partLt(
x',
xs)
partGt[Ite][True][Ite](
False,
x',
Cons(
x,
xs)) →
partGt(
x',
xs)
Types:
quicksort :: Cons:Nil → Cons:Nil
Cons :: S:0' → Cons:Nil → Cons:Nil
part :: S:0' → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
partLt :: S:0' → Cons:Nil → Cons:Nil
partLt[Ite][True][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
< :: S:0' → S:0' → True:False
partGt :: S:0' → Cons:Nil → Cons:Nil
partGt[Ite][True][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
> :: S:0' → S:0' → True:False
app :: Cons:Nil → Cons:Nil → Cons:Nil
notEmpty :: Cons:Nil → True:False
True :: True:False
False :: True:False
goal :: Cons:Nil → Cons:Nil
S :: S:0' → S:0'
0' :: S:0'
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0'2_0 :: S:0'
hole_True:False3_0 :: True:False
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_S:0'5_0 :: Nat → S:0'
Lemmas:
<(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → True, rt ∈ Ω(0)
partLt(gen_S:0'5_0(0), gen_Cons:Nil4_0(n324_0)) → gen_Cons:Nil4_0(0), rt ∈ Ω(1 + n3240)
>(gen_S:0'5_0(n937_0), gen_S:0'5_0(n937_0)) → False, rt ∈ Ω(0)
partGt(gen_S:0'5_0(0), gen_Cons:Nil4_0(n1266_0)) → gen_Cons:Nil4_0(0), rt ∈ Ω(1 + n12660)
Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil4_0(x))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))
No more defined symbols left to analyse.
(30) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
partLt(gen_S:0'5_0(0), gen_Cons:Nil4_0(n324_0)) → gen_Cons:Nil4_0(0), rt ∈ Ω(1 + n3240)
(31) BOUNDS(n^1, INF)
(32) Obligation:
Innermost TRS:
Rules:
quicksort(
Cons(
x,
Cons(
x',
xs))) →
part(
x,
Cons(
x',
xs))
quicksort(
Cons(
x,
Nil)) →
Cons(
x,
Nil)
quicksort(
Nil) →
NilpartLt(
x',
Cons(
x,
xs)) →
partLt[Ite][True][Ite](
<(
x,
x'),
x',
Cons(
x,
xs))
partLt(
x,
Nil) →
NilpartGt(
x',
Cons(
x,
xs)) →
partGt[Ite][True][Ite](
>(
x,
x'),
x',
Cons(
x,
xs))
partGt(
x,
Nil) →
Nilapp(
Cons(
x,
xs),
ys) →
Cons(
x,
app(
xs,
ys))
app(
Nil,
ys) →
ysnotEmpty(
Cons(
x,
xs)) →
TruenotEmpty(
Nil) →
Falsepart(
x,
xs) →
app(
quicksort(
partLt(
x,
xs)),
Cons(
x,
quicksort(
partGt(
x,
xs))))
goal(
xs) →
quicksort(
xs)
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
False>(
S(
x),
S(
y)) →
>(
x,
y)
>(
0',
y) →
False>(
S(
x),
0') →
TruepartLt[Ite][True][Ite](
True,
x',
Cons(
x,
xs)) →
Cons(
x,
partLt(
x',
xs))
partGt[Ite][True][Ite](
True,
x',
Cons(
x,
xs)) →
Cons(
x,
partGt(
x',
xs))
partLt[Ite][True][Ite](
False,
x',
Cons(
x,
xs)) →
partLt(
x',
xs)
partGt[Ite][True][Ite](
False,
x',
Cons(
x,
xs)) →
partGt(
x',
xs)
Types:
quicksort :: Cons:Nil → Cons:Nil
Cons :: S:0' → Cons:Nil → Cons:Nil
part :: S:0' → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
partLt :: S:0' → Cons:Nil → Cons:Nil
partLt[Ite][True][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
< :: S:0' → S:0' → True:False
partGt :: S:0' → Cons:Nil → Cons:Nil
partGt[Ite][True][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
> :: S:0' → S:0' → True:False
app :: Cons:Nil → Cons:Nil → Cons:Nil
notEmpty :: Cons:Nil → True:False
True :: True:False
False :: True:False
goal :: Cons:Nil → Cons:Nil
S :: S:0' → S:0'
0' :: S:0'
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0'2_0 :: S:0'
hole_True:False3_0 :: True:False
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_S:0'5_0 :: Nat → S:0'
Lemmas:
<(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → True, rt ∈ Ω(0)
partLt(gen_S:0'5_0(0), gen_Cons:Nil4_0(n324_0)) → gen_Cons:Nil4_0(0), rt ∈ Ω(1 + n3240)
>(gen_S:0'5_0(n937_0), gen_S:0'5_0(n937_0)) → False, rt ∈ Ω(0)
Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil4_0(x))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))
No more defined symbols left to analyse.
(33) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
partLt(gen_S:0'5_0(0), gen_Cons:Nil4_0(n324_0)) → gen_Cons:Nil4_0(0), rt ∈ Ω(1 + n3240)
(34) BOUNDS(n^1, INF)
(35) Obligation:
Innermost TRS:
Rules:
quicksort(
Cons(
x,
Cons(
x',
xs))) →
part(
x,
Cons(
x',
xs))
quicksort(
Cons(
x,
Nil)) →
Cons(
x,
Nil)
quicksort(
Nil) →
NilpartLt(
x',
Cons(
x,
xs)) →
partLt[Ite][True][Ite](
<(
x,
x'),
x',
Cons(
x,
xs))
partLt(
x,
Nil) →
NilpartGt(
x',
Cons(
x,
xs)) →
partGt[Ite][True][Ite](
>(
x,
x'),
x',
Cons(
x,
xs))
partGt(
x,
Nil) →
Nilapp(
Cons(
x,
xs),
ys) →
Cons(
x,
app(
xs,
ys))
app(
Nil,
ys) →
ysnotEmpty(
Cons(
x,
xs)) →
TruenotEmpty(
Nil) →
Falsepart(
x,
xs) →
app(
quicksort(
partLt(
x,
xs)),
Cons(
x,
quicksort(
partGt(
x,
xs))))
goal(
xs) →
quicksort(
xs)
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
False>(
S(
x),
S(
y)) →
>(
x,
y)
>(
0',
y) →
False>(
S(
x),
0') →
TruepartLt[Ite][True][Ite](
True,
x',
Cons(
x,
xs)) →
Cons(
x,
partLt(
x',
xs))
partGt[Ite][True][Ite](
True,
x',
Cons(
x,
xs)) →
Cons(
x,
partGt(
x',
xs))
partLt[Ite][True][Ite](
False,
x',
Cons(
x,
xs)) →
partLt(
x',
xs)
partGt[Ite][True][Ite](
False,
x',
Cons(
x,
xs)) →
partGt(
x',
xs)
Types:
quicksort :: Cons:Nil → Cons:Nil
Cons :: S:0' → Cons:Nil → Cons:Nil
part :: S:0' → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
partLt :: S:0' → Cons:Nil → Cons:Nil
partLt[Ite][True][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
< :: S:0' → S:0' → True:False
partGt :: S:0' → Cons:Nil → Cons:Nil
partGt[Ite][True][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
> :: S:0' → S:0' → True:False
app :: Cons:Nil → Cons:Nil → Cons:Nil
notEmpty :: Cons:Nil → True:False
True :: True:False
False :: True:False
goal :: Cons:Nil → Cons:Nil
S :: S:0' → S:0'
0' :: S:0'
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0'2_0 :: S:0'
hole_True:False3_0 :: True:False
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_S:0'5_0 :: Nat → S:0'
Lemmas:
<(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → True, rt ∈ Ω(0)
partLt(gen_S:0'5_0(0), gen_Cons:Nil4_0(n324_0)) → gen_Cons:Nil4_0(0), rt ∈ Ω(1 + n3240)
Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil4_0(x))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))
No more defined symbols left to analyse.
(36) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
partLt(gen_S:0'5_0(0), gen_Cons:Nil4_0(n324_0)) → gen_Cons:Nil4_0(0), rt ∈ Ω(1 + n3240)
(37) BOUNDS(n^1, INF)
(38) Obligation:
Innermost TRS:
Rules:
quicksort(
Cons(
x,
Cons(
x',
xs))) →
part(
x,
Cons(
x',
xs))
quicksort(
Cons(
x,
Nil)) →
Cons(
x,
Nil)
quicksort(
Nil) →
NilpartLt(
x',
Cons(
x,
xs)) →
partLt[Ite][True][Ite](
<(
x,
x'),
x',
Cons(
x,
xs))
partLt(
x,
Nil) →
NilpartGt(
x',
Cons(
x,
xs)) →
partGt[Ite][True][Ite](
>(
x,
x'),
x',
Cons(
x,
xs))
partGt(
x,
Nil) →
Nilapp(
Cons(
x,
xs),
ys) →
Cons(
x,
app(
xs,
ys))
app(
Nil,
ys) →
ysnotEmpty(
Cons(
x,
xs)) →
TruenotEmpty(
Nil) →
Falsepart(
x,
xs) →
app(
quicksort(
partLt(
x,
xs)),
Cons(
x,
quicksort(
partGt(
x,
xs))))
goal(
xs) →
quicksort(
xs)
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
False>(
S(
x),
S(
y)) →
>(
x,
y)
>(
0',
y) →
False>(
S(
x),
0') →
TruepartLt[Ite][True][Ite](
True,
x',
Cons(
x,
xs)) →
Cons(
x,
partLt(
x',
xs))
partGt[Ite][True][Ite](
True,
x',
Cons(
x,
xs)) →
Cons(
x,
partGt(
x',
xs))
partLt[Ite][True][Ite](
False,
x',
Cons(
x,
xs)) →
partLt(
x',
xs)
partGt[Ite][True][Ite](
False,
x',
Cons(
x,
xs)) →
partGt(
x',
xs)
Types:
quicksort :: Cons:Nil → Cons:Nil
Cons :: S:0' → Cons:Nil → Cons:Nil
part :: S:0' → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
partLt :: S:0' → Cons:Nil → Cons:Nil
partLt[Ite][True][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
< :: S:0' → S:0' → True:False
partGt :: S:0' → Cons:Nil → Cons:Nil
partGt[Ite][True][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
> :: S:0' → S:0' → True:False
app :: Cons:Nil → Cons:Nil → Cons:Nil
notEmpty :: Cons:Nil → True:False
True :: True:False
False :: True:False
goal :: Cons:Nil → Cons:Nil
S :: S:0' → S:0'
0' :: S:0'
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0'2_0 :: S:0'
hole_True:False3_0 :: True:False
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_S:0'5_0 :: Nat → S:0'
Lemmas:
<(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → True, rt ∈ Ω(0)
Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil4_0(x))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))
No more defined symbols left to analyse.
(39) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(1) was proven with the following lemma:
<(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → True, rt ∈ Ω(0)
(40) BOUNDS(1, INF)